
import daisy.lang._
import Real._


object Traincar4_State9 {
  // f32
  def train4_state9_32(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, s7: Real, s8: Real, y0: Real, y1: Real, y2: Real, y3: Real, y4: Real) = {
    require(-2.5 <= s0 && s0 <= 6.5 && -2.5 <= s1 && s1 <= 6.5 && -2.5 <= s2 && s2 <= 6.5 && -2.5 <= s3 && s3 <= 6.5 && -2 <= s4 && s4 <= 12 &&
      -2 <= s5 && s5 <= 12 && -2 <= s6 && s6 <= 12 && -2 <= s7 && s7 <= 12 && -2 <= s8 && s8 <= 12 &&
      -2 <= y0 && y0 <= 12 && -2 <= y1 && y1 <= 12 && -2 <= y2 && y2 <= 12 && -2 <= y3 && y3 <= 12 && -2 <= y4 && y4 <= 12)
    (-1.73572E-09)*s0 +(-6.90441E-09)*s1+ (1.91831E-08)*s2+ (7.80416E-06)*s3+ (5.01527E-06)*s4+ (-4.73947E-06)*s5+ (4.30545E-07)*s6+
     (3.35281E-05)*s7+ (0.999934)*s8 + (-5.0163739E-06)*y0 + (4.7201386E-06)*y1+ (-4.156438E-07)*y2+ (-3.2406398E-05)*y3+ (6.4987306E-05)*y4+
      (1.4201936E-12)*5.2121094496644555E+03
  } ensuring(res => res +/- 5e-6)

  // 0.5 f32
  def train4_state9_32_05(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, s7: Real, s8: Real, y0: Real, y1: Real, y2: Real, y3: Real, y4: Real) = {
    require(-2.5 <= s0 && s0 <= 6.5 && -2.5 <= s1 && s1 <= 6.5 && -2.5 <= s2 && s2 <= 6.5 && -2.5 <= s3 && s3 <= 6.5 && -2 <= s4 && s4 <= 12 &&
      -2 <= s5 && s5 <= 12 && -2 <= s6 && s6 <= 12 && -2 <= s7 && s7 <= 12 && -2 <= s8 && s8 <= 12 &&
      -2 <= y0 && y0 <= 12 && -2 <= y1 && y1 <= 12 && -2 <= y2 && y2 <= 12 && -2 <= y3 && y3 <= 12 && -2 <= y4 && y4 <= 12)
    (-1.73572E-09)*s0 +(-6.90441E-09)*s1+ (1.91831E-08)*s2+ (7.80416E-06)*s3+ (5.01527E-06)*s4+ (-4.73947E-06)*s5+ (4.30545E-07)*s6+
     (3.35281E-05)*s7+ (0.999934)*s8 + (-5.0163739E-06)*y0 + (4.7201386E-06)*y1+ (-4.156438E-07)*y2+ (-3.2406398E-05)*y3+ (6.4987306E-05)*y4+
      (1.4201936E-12)*5.2121094496644555E+03
  } ensuring(res => res +/- 2.5e-6)

  // 0.1 f32
  def train4_state9_32_01(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, s7: Real, s8: Real, y0: Real, y1: Real, y2: Real, y3: Real, y4: Real) = {
    require(-2.5 <= s0 && s0 <= 6.5 && -2.5 <= s1 && s1 <= 6.5 && -2.5 <= s2 && s2 <= 6.5 && -2.5 <= s3 && s3 <= 6.5 && -2 <= s4 && s4 <= 12 &&
      -2 <= s5 && s5 <= 12 && -2 <= s6 && s6 <= 12 && -2 <= s7 && s7 <= 12 && -2 <= s8 && s8 <= 12 &&
      -2 <= y0 && y0 <= 12 && -2 <= y1 && y1 <= 12 && -2 <= y2 && y2 <= 12 && -2 <= y3 && y3 <= 12 && -2 <= y4 && y4 <= 12)
    (-1.73572E-09)*s0 +(-6.90441E-09)*s1+ (1.91831E-08)*s2+ (7.80416E-06)*s3+ (5.01527E-06)*s4+ (-4.73947E-06)*s5+ (4.30545E-07)*s6+
     (3.35281E-05)*s7+ (0.999934)*s8 + (-5.0163739E-06)*y0 + (4.7201386E-06)*y1+ (-4.156438E-07)*y2+ (-3.2406398E-05)*y3+ (6.4987306E-05)*y4+
      (1.4201936E-12)*5.2121094496644555E+03
  } ensuring(res => res +/- 5e-7)

  // 0.01 f32
  def train4_state9_32_001(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, s7: Real, s8: Real, y0: Real, y1: Real, y2: Real, y3: Real, y4: Real) = {
    require(-2.5 <= s0 && s0 <= 6.5 && -2.5 <= s1 && s1 <= 6.5 && -2.5 <= s2 && s2 <= 6.5 && -2.5 <= s3 && s3 <= 6.5 && -2 <= s4 && s4 <= 12 &&
      -2 <= s5 && s5 <= 12 && -2 <= s6 && s6 <= 12 && -2 <= s7 && s7 <= 12 && -2 <= s8 && s8 <= 12 &&
      -2 <= y0 && y0 <= 12 && -2 <= y1 && y1 <= 12 && -2 <= y2 && y2 <= 12 && -2 <= y3 && y3 <= 12 && -2 <= y4 && y4 <= 12)
    (-1.73572E-09)*s0 +(-6.90441E-09)*s1+ (1.91831E-08)*s2+ (7.80416E-06)*s3+ (5.01527E-06)*s4+ (-4.73947E-06)*s5+ (4.30545E-07)*s6+
     (3.35281E-05)*s7+ (0.999934)*s8 + (-5.0163739E-06)*y0 + (4.7201386E-06)*y1+ (-4.156438E-07)*y2+ (-3.2406398E-05)*y3+ (6.4987306E-05)*y4+
      (1.4201936E-12)*5.2121094496644555E+03
  } ensuring(res => res +/- 5e-8)

  // f64
  def train4_state9_64(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, s7: Real, s8: Real, y0: Real, y1: Real, y2: Real, y3: Real, y4: Real) = {
    require(-2.5 <= s0 && s0 <= 6.5 && -2.5 <= s1 && s1 <= 6.5 && -2.5 <= s2 && s2 <= 6.5 && -2.5 <= s3 && s3 <= 6.5 && -2 <= s4 && s4 <= 12 &&
      -2 <= s5 && s5 <= 12 && -2 <= s6 && s6 <= 12 && -2 <= s7 && s7 <= 12 && -2 <= s8 && s8 <= 12 &&
      -2 <= y0 && y0 <= 12 && -2 <= y1 && y1 <= 12 && -2 <= y2 && y2 <= 12 && -2 <= y3 && y3 <= 12 && -2 <= y4 && y4 <= 12)
    (-1.73572E-09)*s0 +(-6.90441E-09)*s1+ (1.91831E-08)*s2+ (7.80416E-06)*s3+ (5.01527E-06)*s4+ (-4.73947E-06)*s5+ (4.30545E-07)*s6+
     (3.35281E-05)*s7+ (0.999934)*s8 + (-5.0163739E-06)*y0 + (4.7201386E-06)*y1+ (-4.156438E-07)*y2+ (-3.2406398E-05)*y3+ (6.4987306E-05)*y4+
      (1.4201936E-12)*5.2121094496644555E+03
  } ensuring(res => res +/- 9e-15)

  // 0.5 f64
  def train4_state9_64_05(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, s7: Real, s8: Real, y0: Real, y1: Real, y2: Real, y3: Real, y4: Real) = {
    require(-2.5 <= s0 && s0 <= 6.5 && -2.5 <= s1 && s1 <= 6.5 && -2.5 <= s2 && s2 <= 6.5 && -2.5 <= s3 && s3 <= 6.5 && -2 <= s4 && s4 <= 12 &&
      -2 <= s5 && s5 <= 12 && -2 <= s6 && s6 <= 12 && -2 <= s7 && s7 <= 12 && -2 <= s8 && s8 <= 12 &&
      -2 <= y0 && y0 <= 12 && -2 <= y1 && y1 <= 12 && -2 <= y2 && y2 <= 12 && -2 <= y3 && y3 <= 12 && -2 <= y4 && y4 <= 12)
    (-1.73572E-09)*s0 +(-6.90441E-09)*s1+ (1.91831E-08)*s2+ (7.80416E-06)*s3+ (5.01527E-06)*s4+ (-4.73947E-06)*s5+ (4.30545E-07)*s6+
     (3.35281E-05)*s7+ (0.999934)*s8 + (-5.0163739E-06)*y0 + (4.7201386E-06)*y1+ (-4.156438E-07)*y2+ (-3.2406398E-05)*y3+ (6.4987306E-05)*y4+
      (1.4201936E-12)*5.2121094496644555E+03
  } ensuring(res => res +/- 4.5e-15)

  // 0.1 f64
  def train4_state9_64_01(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, s7: Real, s8: Real, y0: Real, y1: Real, y2: Real, y3: Real, y4: Real) = {
    require(-2.5 <= s0 && s0 <= 6.5 && -2.5 <= s1 && s1 <= 6.5 && -2.5 <= s2 && s2 <= 6.5 && -2.5 <= s3 && s3 <= 6.5 && -2 <= s4 && s4 <= 12 &&
      -2 <= s5 && s5 <= 12 && -2 <= s6 && s6 <= 12 && -2 <= s7 && s7 <= 12 && -2 <= s8 && s8 <= 12 &&
      -2 <= y0 && y0 <= 12 && -2 <= y1 && y1 <= 12 && -2 <= y2 && y2 <= 12 && -2 <= y3 && y3 <= 12 && -2 <= y4 && y4 <= 12)
    (-1.73572E-09)*s0 +(-6.90441E-09)*s1+ (1.91831E-08)*s2+ (7.80416E-06)*s3+ (5.01527E-06)*s4+ (-4.73947E-06)*s5+ (4.30545E-07)*s6+
     (3.35281E-05)*s7+ (0.999934)*s8 + (-5.0163739E-06)*y0 + (4.7201386E-06)*y1+ (-4.156438E-07)*y2+ (-3.2406398E-05)*y3+ (6.4987306E-05)*y4+
      (1.4201936E-12)*5.2121094496644555E+03
  } ensuring(res => res +/- 9e-16)

  // 0.01 f64
  def train4_state9_64_001(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, s7: Real, s8: Real, y0: Real, y1: Real, y2: Real, y3: Real, y4: Real) = {
    require(-2.5 <= s0 && s0 <= 6.5 && -2.5 <= s1 && s1 <= 6.5 && -2.5 <= s2 && s2 <= 6.5 && -2.5 <= s3 && s3 <= 6.5 && -2 <= s4 && s4 <= 12 &&
      -2 <= s5 && s5 <= 12 && -2 <= s6 && s6 <= 12 && -2 <= s7 && s7 <= 12 && -2 <= s8 && s8 <= 12 &&
      -2 <= y0 && y0 <= 12 && -2 <= y1 && y1 <= 12 && -2 <= y2 && y2 <= 12 && -2 <= y3 && y3 <= 12 && -2 <= y4 && y4 <= 12)
    (-1.73572E-09)*s0 +(-6.90441E-09)*s1+ (1.91831E-08)*s2+ (7.80416E-06)*s3+ (5.01527E-06)*s4+ (-4.73947E-06)*s5+ (4.30545E-07)*s6+
     (3.35281E-05)*s7+ (0.999934)*s8 + (-5.0163739E-06)*y0 + (4.7201386E-06)*y1+ (-4.156438E-07)*y2+ (-3.2406398E-05)*y3+ (6.4987306E-05)*y4+
      (1.4201936E-12)*5.2121094496644555E+03
  } ensuring(res => res +/- 9e-17)

  // dbldbl
  def train4_state9_dbldbl(s0: Real, s1: Real, s2: Real, s3: Real, s4: Real, s5: Real, s6: Real, s7: Real, s8: Real, y0: Real, y1: Real, y2: Real, y3: Real, y4: Real) = {
    require(-2.5 <= s0 && s0 <= 6.5 && -2.5 <= s1 && s1 <= 6.5 && -2.5 <= s2 && s2 <= 6.5 && -2.5 <= s3 && s3 <= 6.5 && -2 <= s4 && s4 <= 12 &&
      -2 <= s5 && s5 <= 12 && -2 <= s6 && s6 <= 12 && -2 <= s7 && s7 <= 12 && -2 <= s8 && s8 <= 12 &&
      -2 <= y0 && y0 <= 12 && -2 <= y1 && y1 <= 12 && -2 <= y2 && y2 <= 12 && -2 <= y3 && y3 <= 12 && -2 <= y4 && y4 <= 12)
    (-1.73572E-09)*s0 +(-6.90441E-09)*s1+ (1.91831E-08)*s2+ (7.80416E-06)*s3+ (5.01527E-06)*s4+ (-4.73947E-06)*s5+ (4.30545E-07)*s6+
     (3.35281E-05)*s7+ (0.999934)*s8 + (-5.0163739E-06)*y0 + (4.7201386E-06)*y1+ (-4.156438E-07)*y2+ (-3.2406398E-05)*y3+ (6.4987306E-05)*y4+
      (1.4201936E-12)*5.2121094496644555E+03
  } ensuring(res => res +/- 3e-30)

}